Nuprl Definition : rv-unbounded
11,40
postcript
pdf
(
X
(
n
)
as
n
)(
s
) ==
B
:
.
n
:
. (
m
:
. (
n
m
)
B
X
(
m
)(
s
))
latex
Definitions
x
.
A
(
x
)
,
,
x
:
A
.
B
(
x
)
,
x
:
A
.
B
(
x
)
,
,
P
Q
,
A
B
,
r
s
,
f
(
a
)
FDL editor aliases
rv-unbounded
origin
as n)(s) == 
B:
. 
n:
. (m:. (n 
m) 
B X(m)(s)) as n)(s) == B:. n:. (m:. (n m) B X(m)(s)) 
x.A(x)x:A. B(x)x:A. B(x) Q B s